(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 4))
(declare-fun v1 () (_ BitVec 4))
(assert (let ((e2(_ bv2 3)))
(let ((e3(_ bv8 4)))
(let ((e4 (ite (= (_ bv1 1) ((_ extract 2 2) e3)) e3 ((_ sign_extend 1) e2))))
(let ((e5 (ite (= v1 v0) (_ bv1 1) (_ bv0 1))))
(let ((e6 (distinct v0 v1)))
(let ((e7 (= v1 e4)))
(let ((e8 (= e5 e5)))
(let ((e9 (= e3 ((_ zero_extend 3) e5))))
(let ((e10 (= v1 e4)))
(let ((e11 (= ((_ sign_extend 3) e5) v0)))
(let ((e12 (distinct v1 v0)))
(let ((e13 (distinct ((_ sign_extend 2) e5) e2)))
(let ((e14 (ite e10 e8 e9)))
(let ((e15 (xor e7 e14)))
(let ((e16 (xor e12 e12)))
(let ((e17 (ite e11 e13 e11)))
(let ((e18 (= e6 e16)))
(let ((e19 (xor e18 e18)))
(let ((e20 (= e19 e15)))
(let ((e21 (or e20 e20)))
(let ((e22 (xor e21 e21)))
(let ((e23 (or e17 e22)))
e23
)))))))))))))))))))))))

(check-sat)
